COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	DECLARE INDCONST UU
C00010 ENDMK
C⊗;
DECLARE INDCONST UU;
DECLARE INDCONST λ ε SET;
DECLARE INDVAR w w0 w1 w2 w3 w4 z z0 z1 z2 z3 z4;
DECLARE INDVAR a a0 a1 a2 a3 a4 b b0 b1 b2 b3 b4
c c0 c1 c2 c3 c4 d d0 d1 d2 d3 d4 ε SET;
DECLARE INDVAR x x0 x1 x2 x3 x4 y y0 y1 y2 y3 y4
u u0 u1 u2 u3 u4 v v0 v1 v2 v3 v4 ε OBJECT;
DECLARE INDVAR M M0 M1 M2 M3 M4 N N0 N1 N2 N3 N4 ε CLASS;
DECLARE INDVAR m m0 m1 m2 m3 m4 n n0 n1 n2 n3 n4 ε NATNUM;
DECLARE INDVAR p p0 p1 p2 p3 p4 q q0 q1 q2 q3 q4 ε INTEGER;

DECLARE PREDPAR A 1;
DECLARE OPPAR F 1;

DECLARE PREDCONST SET 1;
DECLARE PREDCONST OBJECT 1;
DECLARE PREDCONST CLASS 1;
DECLARE PREDCONST ⊂(CLASS,CLASS)[INF];
DECLARE PREDCONST ε(OBJECT,CLASS) [R←255,L←250];

DECLARE OPCONST ∪(CLASS,CLASS) = CLASS [R←455 L←450];

MOREGENERAL CLASS ≥ {SET}; 
MOREGENERAL OBJECT ≥ {SET}; 

AXIOM OBJECT: ∀w.(OBJECT(w) ⊃ ∃a.(wεa));;
AXIOM CLASS: ∀w.(CLASS(w) ⊃ w=λ ∨ ∃x.(xεw)),
		∀w z.(wεz ⊃ OBJECT(w) ∧ CLASS(z));;
AXIOM SET: ∀w.(SET(w) ≡ CLASS(w) ∧ OBJECT(w));;
AXIOM EXT: ∀M N.(M=N ≡ ∀x.(x ε M ≡ x ε N));;
AXIOM UU: ¬OBJECT(UU) ∧ ¬CLASS(UU);;
AXIOM NULLSET: ∀x.(¬(xελ));;
AXIOM SUBCLASS:	∀M N.(M⊂N ≡ ∀x.(xεM ⊃ xεN)),
		∀M a.(M⊂a ⊃ SET(M));;
AXIOM COMP: ∀x.(x ε {z|A(z)} ≡ A(x));;
AXIOM union: ∀M N x.(x ε (M∪N) ≡ xεM ∨ xεN),
		∀a b. SET(a∪b);;
DECLARE INDCONST V ε CLASS;
AXIOM V: ∀x.(xεV);;
AXIOM UNIT: ∀x.(SET({x}) ∧ ∀y.(yε{x} ≡ y=x));;
AXIOM PAIR:	∀x y.({x,y} = {x}∪{y});;

DEFINE OPAIR:	∀x y.(<x,y> = {{x},{x,y}});;

AXIOM CAR:	∀x y.(x = CAR(<x,y>));;
AXIOM CDR:	∀x y.(y = CDR(<x,y>));;

DECLARE PREDCONST REL FNC 1;
DEFINE REL: ∀M.(REL(M) ≡ ∀z.(zεM ⊃ ∃x y.(z = <x,y>)));;
DEFINE FNC: ∀M.(FNC(M) ≡ REL(M) ∧ ∀x y z.(<x,y>εM ∧ <x,z>εM ⊃ y=z));;

DECLARE INDVAR r r0 r1 r2 s s0 s1 s2εREL,f f0 f1 f2 g g0 g1 g2 h h0 h1 h2εFNC;
DECLARE OPCONST IMAGE(FNC,CLASS)=CLASS;

DEFINE IMAGE: ∀f M.(IMAGE(f,M) = {y|∃x.(xεM ∧ <x,y> ε f)});;
AXIOM KSUBST: ∀f a.SET(IMAGE(f,a));;

DECLARE OPCONST apply(FNC,OBJECT);
AXIOM APPLY:	∀f x.(∃y.(<x,y>εf) ⊃ <x,apply(f,x)>εf);;

DECLARE OPCONST UNION(CLASS)=CLASS[R←1000];
DEFINE UNION: ∀ M.(UNION(M) = {x|∃b.(bεM∧xεb)});;
AXIOM KUNION: ∀a.SET(UNION(a));;

DECLARE OPCONST ∩(CLASS,CLASS)=CLASS[R←555 L←550];
DEFINE inter:	∀M N.(M∩N = {x|xεM ∧ xεN});;
AXIOM kinter: ∀M b.SET(M∩b);;

DECLARE INDCONST SETSεCLASS,natnumsεSET;
DEFINE SETS:	SETS = {x|SET(x)};;

AXIOM REG:	∀M.(¬(M∩SETS=λ) ⊃ ∃a.(aεM ∧ a∩M = λ));;
COMMENT% The above needs fixing - BG.%

AXIOM natnums:	λ ε natnums ∧
∀x.(xεnatnums ⊃ (x∪{x} ε natnums))
∧ ∀M.(λεM ∧ ∀x.(xεM ⊃ x∪{x}εM) ⊃ (natnums ⊂ M)),
	∀x.(NATNUM(x) ≡ xεnatnums);;

AXIOM SETINDUCTION:	∀a.(A(a) ⊃ A(F(a)) ∧ a⊂F(a)) ⊃
∀b.(A(b) ⊃ ∃c.(b⊂c ∧ c=F(c) ∧ A(c) ∧ ∀d.(b⊂d ∧ A(d) ∧ F(d)⊂d ⊃ c⊂d)));;


DECLARE OPCONST ~ 1[PRE];
DEFINE COMPL: ∀M.(~M = {x|¬(xεM)});;

DECLARE OPCONST \ 2[R←355,L←350];
DEFINE DIFF:	∀ M N.(M\N = M ∩ ~N);;

DECLARE OPCONST INTER(CLASS) = CLASS [R←1000];
DEFINE INTER:	∀M.(INTER(M) = {x|∀b.(bεM ⊃ xεb)}),
		∀a.SET(INTER(a));;

DECLARE OPCONST POWER(CLASS)=CLASS;
DEFINE POWER:	∀M.(POWER(M) = {a|a⊂M}),
		∀a.SET(POWER(a));;

DECLARE OPCONST CROSS(CLASS,CLASS)=CLASS;
DEFINE CROSS:	∀M N.(CROSS(M,N) = {a| ∃x y.(xεM ∧ yεN ∧ a = <x,y>)}),
		∀a b.SET(CROSS(a,b));;

DECLARE OPCONST DOM,RNG(FNC)=CLASS,MAPS(CLASS,CLASS)=CLASS,|(FNC,CLASS)=FNC[INF];
DEFINE DOM:	∀f.(DOM(f) = {x|∃y.(<x,y> ε f)}),
		∀f.(SET(f) ⊃ SET(DOM(f)));;
DEFINE RNG:	∀f.(RNG(f) = {y|∃x.(<x,y> ε f)}),
		∀f.(SET(f) ⊃ SET(RNG(f)));;
DEFINE MAPS:	∀M N.(MAPS(M,N) = {f|FNC(f) ∧ DOM(f)=M ∧ RNG(f)=N}),
		∀a b.SET(MAPS(a,b));;
DEFINE RESTR:	∀f M.(f|M = f∩CROSS(M,V)),
		∀f a.SET(f|a);;

DECLARE INDCONST SSETεCLASS;
AXIOM SSET:	∀x.(xεSSET ≡ SET(x) ∧ ∀y.(yεx ⊃ yεSSET));;

DECLARE INDCONST E ON ALEPH0 omega;
DEFINE  E:	  E={c|∃x b.(c=<x,b>∧xεb)};;
DECLARE PREDCONST CONN 2[INF],ORD CARD NATNUM 1,WO(REL,*)[INF],CONG 2;
DECLARE OPCONST   MIN,SUP 1,CONV(REL)=REL,card(*)=ORD;
DEFINE  CONN:	  ∀r M.(r CONN M≡∀x y.(xεM∧yεM⊃<x,y>εr∨<y,x>εr∨x=y));;
DEFINE  ORD:	  ∀a.(ORD(a)≡(aεSSET ∧ E CONN a ∧ ∀b.(bεa⊃b⊂a)));;
DEFINE  ON:	  ON={c|ORD(c)};;
DEFINE  MIN:	  ∀M.(MIN(M)=INTER(ON∩M)∩UNION(ON∩M));;
DEFINE  SUP:	  ∀M.(SUP(M)=MIN({c|ON∩M⊂c}));;
DEFINE  CONV:	  ∀r.(CONV(r)={c|∃x y.(c=<x,y>∧<y,x>εr)});;
DEFINE  CONG:	  ∀M N.(CONG(M,N)≡∃f.(FNC(f)∧FNC(CONV(f))∧DOM(f)=M∧RNG(f)=N));;
DEFINE  CARD:	  ∀a.(CARD(a)≡(aεON∧¬∃b.(bεa∧CONG(a,b))));;
DEFINE  card:	  ∀a.(card(a)=INTER({c|CARD(c)∧CONG(c,a)}));;
DEFINE  WO:	  ∀r a.(r WO a≡((r CONN a)∧
			∀b.(b⊂a∧¬b=λ⊃
			   ∃x.(xεb∧¬∃y.(yεb∧¬y=x∧<y,x>εr)∧∀z.(zεa⊃<z,z>εr)))));;
DEFINE  NATNUM:	  ∀a.(NATNUM(a)≡ORD(a)∧(CONV(E) WO a));;
DEFINE  ALEPH0:	  ALEPH0={c|NATNUM(c)};;
DEFINE  omega:	  omega={c|NATNUM(c)};;
		


AXIOM CHOICE:	∀a.∃b.(bεON ∧ CONG(a,b));;